ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), es:ES, i:Id.
(x:Id. vartype(i;x) r ds(x)?Top)
 (e:E. (loc(e) = i)  (valtype(e) r Valtype(da;kind(e))))
 (n:, e1, e2:{e:E| loc(e) = i} . Dec(ecl-es-halt(es;x)(n,e1,e2))) 

latex

Definitions

ecl-trans-halt2(ds;da;A), {T}, SQType(T), A  B, S  T, Top, {i...j}, False, i  j < k, {i..j}, P  Q, l1 || l2, A, x:A. B(x), , P  Q, P & Q, P  Q, x. t(x), t  T, P  Q, x:A. B(x), Dec(P), , x(s), Valtype(da;k)

Lemmas

decidable not, decidable all int seg, ecl-trans-state wf, ecl-trans-h wf, decidable assert, decidable and, firstn length, decidable int equal, firstn firstn, length firstn, le wf, firstn is iseg, iseg transitivity, ecl-halt-unique, iseg wf, iseg weakening, firstn wf, not wf, ecl-trans wf, ecl-trans-halt2 wf, length wf1, int seg wf, Knd wf, fpf wf, ecl wf, event system wf, top wf, id-deq wf, fpf-cap wf, es-vartype wf, es-kind wf, ma-valtype wf, es-valtype wf, nat wf, es-loc wf, Id wf, es-E wf, ecl-trans-property, event-info wf, ecl-es-halt-ecl-halt, es-hist wf, ecl-halt wf, ecl-es-halt wf, decidable functionality